acea103cb22b5de3a3cce78a8f89f08373123d2f,src/org/sosy_lab/solver/test/UfEliminationTest.java,UfEliminationTest,nestedUfs,#,103
Before Change
BooleanFormula f = bmgr.xor(f1, f2);
BooleanFormula argsEqual = bmgr.and(v1EqualsV2, v3EqualsV4);
BooleanFormula withOutUfs = ackermannization.eliminateUfs(f).getFormula();
assertThatFormula(f).isSatisfiable(); // sanity check
assertThatFormula(withOutUfs).isSatisfiable();
assertThatFormula(bmgr.and(argsEqual, f)).isUnsatisfiable(); // sanity check
After Change
BooleanFormula f = bmgr.xor(f1, f2);
BooleanFormula argsEqual = bmgr.and(v1EqualsV2, v3EqualsV4);
BooleanFormula withOutUfs = ackermannization.eliminateUfs(f);
assertThatFormula(f).isSatisfiable(); // sanity check
assertThatFormula(withOutUfs).isSatisfiable();
assertThatFormula(bmgr.and(argsEqual, f)).isUnsatisfiable(); // sanity check